\begin{tabbing}
$\forall$$T$:Type, ${\it as}$:$T$ List, $f$, $g$:($T$$\rightarrow\mathbb{B}$).
\\[0ex](\=priority{-}select($f$;$g$;${\it as}$) $=$ inl(true$_{2}$) $\in$ $\mathbb{B}$+Unit\+
\\[0ex]$\Leftrightarrow$
\\[0ex]($\exists$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it as}$$\parallel$}}$. $f$(${\it as}$[$i$]) \& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$i$}}$. $\neg$$g$(${\it as}$[$j$]))))
\-\\[0ex]\& (\=priority{-}select($f$;$g$;${\it as}$) $=$ inl(false$_{2}$) $\in$ $\mathbb{B}$+Unit\+
\\[0ex]$\Leftrightarrow$
\\[0ex]($\exists$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it as}$$\parallel$}}$. $g$(${\it as}$[$i$]) \& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$i$+1}}$. $\neg$$f$(${\it as}$[$j$]))))
\-\\[0ex]\& (priority{-}select($f$;$g$;${\it as}$) $=$ inr($\cdot$) $\in$ $\mathbb{B}$+Unit $\Leftrightarrow$ ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it as}$$\parallel$}}$. $\neg$$f$(${\it as}$[$i$]) \& $\neg$$g$(${\it as}$[$i$])))
\end{tabbing}